package it.unicam.fishpass.prism;

//import it.unicam.fishpass.prism.Declaration;
//import it.unicam.fishpass.prism.MDPGraph;
//import it.unicam.fishpass.prism.MultiArc;

//import it.unicam.fishpass.prism.Module;

import it.unicam.fishpass.prism.editor.EditorAboutFrame;
import it.unicam.fishpass.prism.editor.EditorKeyboardHandler;
import it.unicam.fishpass.prism.editor.EditorPalette;
import it.unicam.fishpass.prism.editor.EditorPopupMenu;
import it.unicam.fishpass.prism.editor.EditorToolBar;
import it.unicam.fishpass.prism.parser.EPDTA2PRISM;

import java.awt.BorderLayout;
import java.awt.Point;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.awt.event.ComponentAdapter;
import java.awt.event.MouseAdapter;
import java.awt.event.MouseEvent;
import java.awt.event.MouseMotionListener;
import java.awt.event.MouseWheelEvent;
import java.awt.event.MouseWheelListener;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.concurrent.ExecutionException;

import javax.swing.AbstractAction;
import javax.swing.Action;
import javax.swing.BorderFactory;
import javax.swing.ImageIcon;
import javax.swing.JCheckBoxMenuItem;
import javax.swing.JFrame;
import javax.swing.JLabel;
import javax.swing.JMenuBar;
import javax.swing.JOptionPane;
import javax.swing.JPanel;
import javax.swing.JPopupMenu;
import javax.swing.JSplitPane;
import javax.swing.JTabbedPane;
import javax.swing.SwingConstants;
import javax.swing.SwingUtilities;
import javax.swing.SwingWorker;
import javax.swing.UIManager;

import com.mxgraph.layout.mxCircleLayout;
import com.mxgraph.layout.mxCompactTreeLayout;
import com.mxgraph.layout.mxEdgeLabelLayout;
import com.mxgraph.layout.mxIGraphLayout;
import com.mxgraph.layout.mxOrganicLayout;
import com.mxgraph.layout.mxParallelEdgeLayout;
import com.mxgraph.layout.mxPartitionLayout;
import com.mxgraph.layout.mxStackLayout;
import com.mxgraph.layout.hierarchical.mxHierarchicalLayout;
import com.mxgraph.model.mxCell;
import com.mxgraph.swing.mxGraphComponent;
import com.mxgraph.swing.mxGraphOutline;
import com.mxgraph.swing.handler.mxKeyboardHandler;
import com.mxgraph.swing.handler.mxRubberband;
import com.mxgraph.swing.util.mxMorphing;
import com.mxgraph.util.mxEvent;
import com.mxgraph.util.mxEventObject;
import com.mxgraph.util.mxRectangle;
import com.mxgraph.util.mxResources;
import com.mxgraph.util.mxUndoManager;
import com.mxgraph.util.mxUndoableEdit;
import com.mxgraph.util.mxEventSource.mxIEventListener;
import com.mxgraph.util.mxUndoableEdit.mxUndoableChange;
import com.mxgraph.view.mxGraph;

public class BasicGraphEditor extends JPanel {

	/** Auto-generated serialization ID */
	private static final long serialVersionUID = -6561623072112577140L;

	/** Adds required resources for i18n */
	static {
		try {
			mxResources.add("resources.editor");
		} catch (Exception e) {
			System.err.println(e.getMessage());
		}
	}

	/**
	 * 
	 */
	protected static mxGraphComponent graphComponent;

	/**
	 * 
	 */
	protected mxGraphOutline graphOutline;
	/**
	 * 
	 */
	protected JTabbedPane libraryPane;

	/**
	 * 
	 */
	protected mxUndoManager undoManager;

	/**
	 * 
	 */
	protected String appTitle;

	/**
	 * 
	 */
	protected JLabel statusBar;

	/**
	 * 
	 */
	public File currentFile;

	/**
	 * Flag indicating whether the current graph has been modified
	 */
	protected boolean modified = false;

	/**
	 * 
	 */
	protected mxRubberband rubberband;
	private EditorToolBar toolbar;

	/**
	 * 
	 */
	protected mxKeyboardHandler keyboardHandler;

	/**
	 * 
	 */
	protected mxIEventListener undoHandler = new mxIEventListener() {
		@Override
		public void invoke(Object source, mxEventObject evt) {
			undoManager.undoableEditHappened((mxUndoableEdit) evt
					.getProperty("edit"));
		}
	};

	/**
	 * 
	 */
	protected mxIEventListener changeTracker = new mxIEventListener() {
		@Override
		public void invoke(Object source, mxEventObject evt) {
			setModified(true);
		}
	};

	/**
	 * 
	 */
	public BasicGraphEditor(String appTitle, mxGraphComponent component) {
		// Stores and updates the frame title
		this.appTitle = appTitle;

		// Stores a reference to the graph and creates the command history
		graphComponent = component;
		final mxGraph graph = graphComponent.getGraph();
		undoManager = createUndoManager();

		// Do not change the scale and translation after files have been loaded
		graph.setResetViewOnRootChange(false);

		// Updates the modified flag if the graph model changes
		graph.getModel().addListener(mxEvent.CHANGE, changeTracker);

		// Adds the command history to the model and view
		graph.getModel().addListener(mxEvent.UNDO, undoHandler);
		graph.getView().addListener(mxEvent.UNDO, undoHandler);

		// Keeps the selection in sync with the command history
		mxIEventListener undoHandler = new mxIEventListener() {
			@Override
			public void invoke(Object source, mxEventObject evt) {
				List<mxUndoableChange> changes = ((mxUndoableEdit) evt
						.getProperty("edit")).getChanges();
				graph.setSelectionCells(graph
						.getSelectionCellsForChanges(changes));
			}
		};

		undoManager.addListener(mxEvent.UNDO, undoHandler);
		undoManager.addListener(mxEvent.REDO, undoHandler);

		// Creates the graph outline component
		graphOutline = new mxGraphOutline(graphComponent);

		// Creates the library pane that contains the tabs with the palettes
		libraryPane = new JTabbedPane();

		// Creates the inner split pane that contains the library with the
		// palettes and the graph outline on the left side of the window
		JSplitPane inner = new JSplitPane(JSplitPane.VERTICAL_SPLIT,
				libraryPane, graphOutline);
		inner.setDividerLocation(100);
		inner.setResizeWeight(1);
		inner.setDividerSize(6);
		inner.setBorder(null);

		// Creates the outer split pane that contains the inner split pane and
		// the graph component on the right side of the window
		JSplitPane outer = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, inner,
				graphComponent);
		outer.setOneTouchExpandable(true);
		outer.setDividerLocation(200);
		outer.setDividerSize(6);
		outer.setBorder(null);

		// Creates the status bar
		statusBar = createStatusBar();

		// Display some useful information about repaint events
		installRepaintListener();

		// Puts everything together
		setLayout(new BorderLayout());
		add(outer, BorderLayout.CENTER);
		add(statusBar, BorderLayout.SOUTH);
		installToolBar();

		// Installs rubberband selection and handling for some special
		// keystrokes such as F2, Control-C, -V, X, A etc.
		installHandlers();
		installListeners();
		updateTitle();
	}

	/**
	 * 
	 */
	protected mxUndoManager createUndoManager() {
		return new mxUndoManager();
	}

	/**
	 * 
	 */
	protected void installHandlers() {
		rubberband = new mxRubberband(graphComponent);
		keyboardHandler = new EditorKeyboardHandler(graphComponent);
	}

	/**
	 * 
	 */
	protected void installToolBar() {
		add(toolbar = new EditorToolBar(this, SwingConstants.HORIZONTAL),
				BorderLayout.NORTH);
	}

	/**
	 * 
	 */
	protected JLabel createStatusBar() {
		JLabel statusBar = new JLabel(mxResources.get("ready"));
		statusBar.setBorder(BorderFactory.createEmptyBorder(2, 4, 2, 4));

		return statusBar;
	}

	/**
	 * 
	 */
	protected void installRepaintListener() {
		graphComponent.getGraph().addListener(mxEvent.REPAINT,
				new mxIEventListener() {
					@Override
					public void invoke(Object source, mxEventObject evt) {
						String buffer = (graphComponent.getTripleBuffer() != null) ? ""
								: " (unbuffered)";
						mxRectangle dirty = (mxRectangle) evt
								.getProperty("region");

						if (dirty == null) {
							status("Repaint all" + buffer);
						} else {
							status("Repaint: x=" + (int) (dirty.getX()) + " y="
									+ (int) (dirty.getY()) + " w="
									+ (int) (dirty.getWidth()) + " h="
									+ (int) (dirty.getHeight()) + buffer);
						}
					}
				});
	}

	/**
	 * 
	 */
	public EditorPalette insertPalette(String title) {
		final EditorPalette palette = new EditorPalette();
		libraryPane.add(title, palette);

		// Updates the widths of the palettes if the container size changes
		libraryPane.addComponentListener(new ComponentAdapter() {
			/**
			 * 
			 */

		});

		return palette;
	}

	/**
	 * 
	 */
	protected void mouseWheelMoved(MouseWheelEvent e) {
		if (e.getWheelRotation() < 0) {
			graphComponent.zoomIn();
		} else {
			graphComponent.zoomOut();
		}

		status(mxResources.get("scale") + ": "
				+ (int) (100 * graphComponent.getGraph().getView().getScale())
				+ "%");
	}

	/**
	 * 
	 */
	protected void showOutlinePopupMenu(MouseEvent e) {
		Point pt = SwingUtilities.convertPoint(e.getComponent(), e.getPoint(),
				graphComponent);
		JCheckBoxMenuItem item = new JCheckBoxMenuItem(
				mxResources.get("magnifyPage"));
		item.setSelected(graphOutline.isFitPage());

		item.addActionListener(new ActionListener() {
			/**
			 * 
			 */
			@Override
			public void actionPerformed(ActionEvent e) {
				graphOutline.setFitPage(!graphOutline.isFitPage());
				graphOutline.repaint();
			}
		});

		JCheckBoxMenuItem item2 = new JCheckBoxMenuItem(
				mxResources.get("showLabels"));
		item2.setSelected(graphOutline.isDrawLabels());

		item2.addActionListener(new ActionListener() {

			@Override
			public void actionPerformed(ActionEvent e) {
				graphOutline.setDrawLabels(!graphOutline.isDrawLabels());
				graphOutline.repaint();
			}
		});

		JCheckBoxMenuItem item3 = new JCheckBoxMenuItem(
				mxResources.get("buffering"));
		item3.setSelected(graphOutline.isTripleBuffered());

		item3.addActionListener(new ActionListener() {

			@Override
			public void actionPerformed(ActionEvent e) {
				graphOutline.setTripleBuffered(!graphOutline.isTripleBuffered());
				graphOutline.repaint();
			}
		});

		JPopupMenu menu = new JPopupMenu();
		menu.add(item);
		menu.add(item2);
		menu.add(item3);
		menu.show(graphComponent, pt.x, pt.y);

		e.consume();
	}

	/**
	 * 
	 */
	protected void showGraphPopupMenu(MouseEvent e) {
		Point pt = SwingUtilities.convertPoint(e.getComponent(), e.getPoint(),
				graphComponent);
		EditorPopupMenu menu = new EditorPopupMenu(BasicGraphEditor.this);
		menu.show(graphComponent, pt.x, pt.y);

		e.consume();
	}

	/**
	 * 
	 */
	protected void mouseLocationChanged(MouseEvent e) {
		status(e.getX() + ", " + e.getY());
	}

	/**
	 * 
	 */
	protected void installListeners() {
		// Installs mouse wheel listener for zooming
		MouseWheelListener wheelTracker = new MouseWheelListener() {

			@Override
			public void mouseWheelMoved(MouseWheelEvent e) {
				if (e.getSource() instanceof mxGraphOutline
						|| e.isControlDown()) {
					BasicGraphEditor.this.mouseWheelMoved(e);
				}
			}

		};

		// Handles mouse wheel events in the outline and graph component
		graphOutline.addMouseWheelListener(wheelTracker);
		graphComponent.addMouseWheelListener(wheelTracker);

		// Installs the popup menu in the outline
		graphOutline.addMouseListener(new MouseAdapter() {

			@Override
			public void mousePressed(MouseEvent e) {
				// Handles context menu on the Mac where the trigger is on
				// mousepressed
				mouseReleased(e);
			}

			@Override
			public void mouseReleased(MouseEvent e) {
				if (e.getButton() == MouseEvent.BUTTON3) {
					showOutlinePopupMenu(e);
				}
			}

		});

		// Installs the popup menu in the graph component
		graphComponent.getGraphControl().addMouseListener(new MouseAdapter() {

			@Override
			public void mousePressed(MouseEvent e) {
				if (e.getButton() == MouseEvent.BUTTON3)
					showGraphPopupMenu(e);
			}

			@Override
			public void mouseClicked(MouseEvent e) {
				if (e.getButton() == MouseEvent.BUTTON1) { // LEFT BUTTON
					// NOTE DOES NOTHING
				}
			}

		});

		// Installs a mouse motion listener to display the mouse location
		graphComponent.getGraphControl().addMouseMotionListener(
				new MouseMotionListener() {

					@Override
					public void mouseDragged(MouseEvent e) {
						mouseLocationChanged(e);
					}

					@Override
					public void mouseMoved(MouseEvent e) {
						mouseDragged(e);
					}

				});
	}

	/**
	 * 
	 */
	public void setCurrentFile(File file) {
		File oldValue = currentFile;
		currentFile = file;

		firePropertyChange("currentFile", oldValue, file);

		if (oldValue != file) {
			updateTitle();
		}
	}

	/**
	 * 
	 */
	public File getCurrentFile() {
		return currentFile;
	}

	/**
	 * 
	 * @param modified
	 */
	public void setModified(boolean modified) {
		boolean oldValue = this.modified;
		this.modified = modified;

		firePropertyChange("modified", oldValue, modified);

		if (oldValue != modified) {
			updateTitle();
		}
	}

	/**
	 * 
	 * @return whether or not the current graph has been modified
	 */
	public boolean isModified() {
		return modified;
	}

	/**
	 * 
	 */
	public static mxGraphComponent getGraphComponent() {
		return graphComponent;
	}

	/**
	 * 
	 */
	public mxGraphOutline getGraphOutline() {
		return graphOutline;
	}

	/**
	 * 
	 */
	public JTabbedPane getLibraryPane() {
		return libraryPane;
	}

	/**
	 * 
	 */
	public mxUndoManager getUndoManager() {
		return undoManager;
	}

	/**
	 * 
	 * @param name
	 * @param action
	 * @return a new Action bound to the specified string name
	 */
	public Action bind(String name, final Action action) {
		return bind(name, action, null);
	}

	/**
	 * 
	 * @param name
	 * @param action
	 * @return a new Action bound to the specified string name and icon
	 */
	@SuppressWarnings("serial")
	public Action bind(String name, final Action action, String iconUrl) {
		AbstractAction newAction = new AbstractAction(name,
				(iconUrl != null) ? new ImageIcon(
						BasicGraphEditor.class.getResource(iconUrl)) : null) {
			@Override
			public void actionPerformed(ActionEvent e) {
				action.actionPerformed(new ActionEvent(getGraphComponent(), e
						.getID(), e.getActionCommand()));
			}
		};

		newAction.putValue(Action.SHORT_DESCRIPTION,
				action.getValue(Action.SHORT_DESCRIPTION));

		return newAction;
	}

	/**
	 * 
	 * @param msg
	 */
	public void status(String msg) {
		statusBar.setText(msg);
	}

	/**
	 * 
	 */
	public void updateTitle() {
		JFrame frame = (JFrame) SwingUtilities.windowForComponent(this);

		if (frame != null) {
			String title = (currentFile != null) ? currentFile
					.getAbsolutePath() : mxResources.get("newDiagram");

			if (modified) {
				title += "*";
			}

			frame.setTitle(title + " - " + appTitle);
		}
	}

	/**
	 * 
	 */
	public void about() {
		JFrame frame = (JFrame) SwingUtilities.windowForComponent(this);

		if (frame != null) {
			EditorAboutFrame about = new EditorAboutFrame(frame);
			about.setModal(true);

			// Centers inside the application frame
			int x = frame.getX() + (frame.getWidth() - about.getWidth()) / 2;
			int y = frame.getY() + (frame.getHeight() - about.getHeight()) / 2;
			about.setLocation(x, y);

			// Shows the modal dialog and waits
			about.setVisible(true);
		}
	}

	/**
	 * 
	 */
	public void exit() {
		JFrame frame = (JFrame) SwingUtilities.windowForComponent(this);

		if (frame != null) {
			frame.dispose();
		}
	}

	/**
	 * 
	 */
	public void setLookAndFeel(String clazz) {
		JFrame frame = (JFrame) SwingUtilities.windowForComponent(this);

		if (frame != null) {
			try {
				UIManager.setLookAndFeel(clazz);
				SwingUtilities.updateComponentTreeUI(frame);

				// Needs to assign the key bindings again
				keyboardHandler = new EditorKeyboardHandler(graphComponent);
			} catch (Exception e1) {
				e1.printStackTrace();
			}
		}
	}

	/**
	 * 
	 */
	public JFrame createFrame(JMenuBar menuBar) {
		JFrame frame = new JFrame();
		frame.getContentPane().add(this);
		frame.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE);
		frame.setJMenuBar(menuBar);
		frame.setSize(1024, 650);
		frame.setLocationRelativeTo(null);
		// Updates the frame title
		updateTitle();

		return frame;
	}

	/**
	 * Creates an action that executes the specified layout.
	 * 
	 * @param key
	 *            Key to be used for getting the label from mxResources and also
	 *            to create the layout instance for the commercial graph editor
	 *            example.
	 * @return an action that executes the specified layout
	 */
	@SuppressWarnings("serial")
	public Action graphLayout(final String key, boolean animate) {
		final mxIGraphLayout layout = createLayout(key, animate);

		if (layout != null)
			return new AbstractAction(mxResources.get(key)) {
				@Override
				public void actionPerformed(ActionEvent e) {
					final mxGraph graph = graphComponent.getGraph();
					Object cell = graph.getSelectionCell();

					if (cell == null
							|| graph.getModel().getChildCount(cell) == 0) {
						cell = graph.getDefaultParent();
					}

					graph.getModel().beginUpdate();
					try {
						long t0 = System.currentTimeMillis();
						layout.execute(cell);
						status("Layout: " + (System.currentTimeMillis() - t0)
								+ " ms");
					} finally {
						mxMorphing morph = new mxMorphing(graphComponent, 20,
								1.2, 20);

						morph.addListener(mxEvent.DONE, new mxIEventListener() {

							@Override
							public void invoke(Object sender, mxEventObject evt) {
								graph.getModel().endUpdate();
							}

						});

						morph.startAnimation();
					}

				}

			};
		// else
		return new AbstractAction(mxResources.get(key)) {

			@Override
			public void actionPerformed(ActionEvent e) {
				JOptionPane.showMessageDialog(graphComponent,
						mxResources.get("noLayout"));
			}

		};

	}

	/**
	 * Creates a layout instance for the given identifier.
	 * 
	 * @param animate
	 *            Unused in the base case
	 */
	protected mxIGraphLayout createLayout(String ident, boolean animate) {
		mxIGraphLayout layout = null;

		if (ident != null) {
			mxGraph graph = graphComponent.getGraph();

			if (ident.equals("verticalHierarchical")) {
				layout = new mxHierarchicalLayout(graph);
			} else if (ident.equals("horizontalHierarchical")) {
				layout = new mxHierarchicalLayout(graph, SwingConstants.WEST);
			} else if (ident.equals("verticalTree")) {
				layout = new mxCompactTreeLayout(graph, false);
			} else if (ident.equals("horizontalTree")) {
				layout = new mxCompactTreeLayout(graph, true);
			} else if (ident.equals("parallelEdges")) {
				layout = new mxParallelEdgeLayout(graph);
			} else if (ident.equals("placeEdgeLabels")) {
				layout = new mxEdgeLabelLayout(graph);
			} else if (ident.equals("organicLayout")) {
				layout = new mxOrganicLayout(graph);
			}
			if (ident.equals("verticalPartition")) {
				layout = new mxPartitionLayout(graph, false) {
					/**
					 * Overrides the empty implementation to return the size of
					 * the graph control.
					 */

					@Override
					public mxRectangle getContainerSize() {
						return graphComponent.getLayoutAreaSize();
					}
				};
			} else if (ident.equals("horizontalPartition")) {
				layout = new mxPartitionLayout(graph, true) {
					/**
					 * Overrides the empty implementation to return the size of
					 * the graph control.
					 */
					@Override
					public mxRectangle getContainerSize() {
						return graphComponent.getLayoutAreaSize();
					}
				};
			} else if (ident.equals("verticalStack")) {
				layout = new mxStackLayout(graph, false) {
					/**
					 * Overrides the empty implementation to return the size of
					 * the graph control.
					 */
					@Override
					public mxRectangle getContainerSize() {
						return graphComponent.getLayoutAreaSize();
					}
				};
			} else if (ident.equals("horizontalStack")) {
				layout = new mxStackLayout(graph, true) {
					/**
					 * Overrides the empty implementation to return the size of
					 * the graph control.
					 */
					@Override
					public mxRectangle getContainerSize() {
						return graphComponent.getLayoutAreaSize();
					}
				};
			} else if (ident.equals("circleLayout")) {
				layout = new mxCircleLayout(graph);
			}
		}

		return layout;
	}

	public void doInBackground() {
		toolbar.setButtonStatus(false);
		SwingWorker<Boolean, Void> worker = new SwingWorker<Boolean, Void>() {
			@Override
			public Boolean doInBackground() {
				// build the intermediate file
				mxGraph g = graphComponent.getGraph();
				Object[] vertexes = g.getChildVertices(g.getDefaultParent());
				Object[] edges = g.getChildEdges(g.getDefaultParent());
				if (vertexes.length == 0 || edges.length == 0)
					return new Boolean(false);
				// build the final output
				StringBuilder sb = new StringBuilder("automaton\nmaxtime = "
						+ getMaxTime() + "\n");
				//
				// ArrayList<String> locs = new ArrayList<String>();
				ArrayList<mxCell> ellipses = new ArrayList<mxCell>();
				String locz = "";
				for (Object o : vertexes) {
					mxCell cell = (mxCell) o;
					if (cell.getStyle() == null) {
						String temp;
						if ((temp = cell.getValue().toString().trim())
								.isEmpty())
							return new Boolean(false); // LOCATION IS EMPTY!!
						int index = temp.indexOf('\n');
						if (index > 0 && index != temp.lastIndexOf('\n')) {
							temp = temp.substring(0, temp.lastIndexOf('\n'));
							temp = temp.replace('\n', '|');
							temp = temp.replace('&', '^');
							locz = temp.substring(0, index)
									+ (locz.isEmpty() ? "" : ", " + locz);
						} else if (index > 0) {
							temp = temp.replace('\n', '|');
							temp = temp.replace('&', '^');
							locz = locz + ", " + temp.substring(0, index);
						} else
							locz = locz + ", " + temp;
						// locs.add("[" + temp + "]");
					} else
						ellipses.add(cell);
				}
				if (!locz.isEmpty())
					sb.append("#NODE_DEC\n" + locz + ";\n");
				else
					sb.append("\n");
				HashSet<String> tempString = new HashSet<String>();
				for (mxCell cur : ellipses) {
					for (Object o : edges) {
						mxCell cell = (mxCell) o;
						if (cell.getTarget() == cur) {
							String temp;
							if ((temp = cell.getValue().toString().trim())
									.isEmpty())
								return new Boolean(false);
							if (temp.contains("\n"))
								temp = temp.split("\n")[1];
							// else transition is NOT empty
							String clockConstraint = temp.substring(
									temp.indexOf('('), temp.indexOf(')'));
							String[] dataRow = clockConstraint.split("&");
							for (String constraint : dataRow) {
								int minusInd = -1;
								if ((minusInd = constraint.indexOf('-')) != -1) {
									tempString.add(constraint
											.substring(0, minusInd).trim()
											.replace("(", "").replace(")", ""));
									int opInd = -1;
									opInd = constraint.indexOf('<');
									if (opInd == -1)
										opInd = constraint.indexOf('>');
									if (opInd == -1)
										opInd = constraint.indexOf('=');
									if (opInd == -1)
										return new Boolean(false);
									tempString.add(constraint
											.substring(minusInd + 1, opInd)
											.trim().replace("(", "")
											.replace(")", ""));
								} else { // a # num
									int opInd = -1;
									opInd = constraint.indexOf('<');
									if (opInd == -1)
										opInd = constraint.indexOf('>');
									if (opInd == -1)
										opInd = constraint.indexOf('=');
									if (opInd == -1)
										return new Boolean(false);
									tempString.add(constraint
											.substring(0, opInd).trim()
											.replace("(", "").replace(")", ""));
								}
							}
							break;
						}
					}
				}
				for (Object o : vertexes) {
					mxCell cell = (mxCell) o;
					if (!cell.getValue().toString().contains("\n"))
						continue;
					// else contains invariants
					String invariant = cell.getValue().toString().trim()
							.split("\n")[1];
					String[] dataRow = invariant.split("&");
					for (String constraint : dataRow) {
						int minusInd = -1;
						if ((minusInd = constraint.indexOf('-')) != -1) {
							tempString.add(constraint.substring(0, minusInd)
									.trim().replace("(", "").replace(")", ""));
							int opInd = -1;
							opInd = constraint.indexOf('<');
							if (opInd == -1)
								opInd = constraint.indexOf('>');
							if (opInd == -1)
								opInd = constraint.indexOf('=');
							if (opInd == -1)
								return new Boolean(false);
							tempString.add(constraint
									.substring(minusInd + 1, opInd).trim()
									.replace("(", "").replace(")", ""));
						} else { // a # num
							int opInd = -1;
							opInd = constraint.indexOf('<');
							if (opInd == -1)
								opInd = constraint.indexOf('>');
							if (opInd == -1)
								opInd = constraint.indexOf('=');
							if (opInd == -1)
								return new Boolean(false);
							tempString.add(constraint.substring(0, opInd)
									.trim().replace("(", "").replace(")", ""));
						}
					}
					break;
				}
				if (!tempString.isEmpty()) {
					sb.append("#CLOCK_DEC\n");
					for (String clock : tempString) {
						sb.append(clock + " = [0.0 .. +INF] init 0.0, ");
					}
					sb.replace(sb.length() - 2, sb.length(), ";\n");
				} else
					sb.append("\n");
				//
				StringBuilder sbExpr = new StringBuilder();
				for (Object o : edges) {
					mxCell cell = (mxCell) o;
					String temp = cell.getValue().toString().trim();
					if (cell.getSource().getStyle() == null)
						sbExpr.append(temp.substring(temp.lastIndexOf('(') + 1,
								temp.lastIndexOf(')')).replace('&', '^')
								+ ";");
					else
						sbExpr.append(temp.substring(temp.indexOf('[') + 1,
								temp.indexOf(']')) + ";");
				}
				ExpressionParser p = new ExpressionParser();
				if (p.checkExpressions(sbExpr.toString())) {
					System.out
							.println("Parsing correctly done");
				} else {
					
					return new Boolean(false);
				}
				if (!p.getBoolVars().isEmpty() || !p.getIntVars().isEmpty()) {
					sb.append("#VARIABLE_DEC\n");
					for (String bool : p.getBoolVars())
						if (!tempString.contains(bool))
							sb.append(bool.trim().toUpperCase() + " = bool init false, ");
					
					for (String var : p.getIntVars())
						if (!tempString.contains(var))
							sb.append(var.replace('[', ' ').trim()
									.toUpperCase()
									+ " = 0.0, ");
					sb.replace(sb.length() - 2, sb.length(), ";\n"); // ',' --->
				} else
					sb.append("\n");
				tempString.clear();
				//
				// TRANSITIONS
				for (mxCell cur : ellipses) {
					String guard = "";
					boolean isUrgent = false;
					mxCell source = null;
					for (Object o : edges) {
						mxCell cell = (mxCell) o;
						if (cell.getTarget() == cur) {
							source = (mxCell) cell.getSource();
							String[] values = cell.getValue().toString().trim()
									.split("\n");
							for (String ss : values) {
								if (!ss.equalsIgnoreCase("U"))
									guard += " " + ss;
								else
									isUrgent = true;
							}
							break;
						}
					}
					guard = guard.replace('&', '^').replace('(', ' ')
							.replace(')', ' ');
					//
					String edgesString = "";
					for (Object o : edges) {
						mxCell cell = (mxCell) o;
						if (cell.getSource() == cur) {
							edgesString += "(" + guard.trim() + ") ";
							String[] data = cell.getValue().toString()
									.split("\n");
							if (!data[0].contains("."))
								edgesString += data[0] + ".0 ";
							else
								edgesString += data[0] + " ";
							edgesString += " "
									+ cell.getTarget().getValue().toString()
											.split("\n")[0] + " ";
							String cr = data[1].trim().replace("\n", "")
									.replace('&', '^');
							edgesString += cr + " + ";
						}
					}
					//
					if (source != null) {
						String sourceString = source.getValue().toString()
								.trim();
						if (sourceString.indexOf("\n") > 0
								&& sourceString.indexOf("\n") != sourceString
										.lastIndexOf('\n'))
							sourceString = sourceString.substring(0,
									sourceString.lastIndexOf("\n"));
						sourceString = sourceString.replace("\n", " | ");
						sourceString = sourceString.replace('&', '^');
						sb.append("[" + sourceString + "]"
								+ (isUrgent ? " -U> " : " -> ") + edgesString);
						sb.replace(sb.length() - 3, sb.length(), "\n");
					} else
						return new Boolean(false);
				}
				//
				sb.append("endautomaton\n");
				//
				FileWriter f = null;
				try {
					f = new FileWriter(currentFile.getParent()
							+ File.separator
							+ currentFile.getName().substring(0,
									currentFile.getName().indexOf('.'))
							+ ".int");
					f.append(sb);
				} catch (IOException e) {
					e.printStackTrace();
					return new Boolean(false);
				} finally {
					if (f != null)
						try {
							f.close();
						} catch (IOException e) {
							e.printStackTrace();
						}
				}
				return new Boolean(true);
			}

			@Override
			public void done() {
				try {
					if (!get().booleanValue())
						System.err.println("bad termination");
					else {
						EPDTA2PRISM.parse(currentFile.getParent()
								+ File.separator
								+ currentFile.getName().substring(0,
										currentFile.getName().indexOf('.'))
								+ ".int");
					}
				} catch (InterruptedException | ExecutionException e) {
					e.printStackTrace();
				}
				setButtonStatus(true);
			}
		};
		worker.execute();
	}

	String getMaxTime() {
		return toolbar.getMaxTime();
	}

	void setButtonStatus(boolean status) {
		toolbar.setButtonStatus(status);
	}

}
